(DEFPROP REENTER 
 (LAMBDA NIL
  (PROG (Z1 Z2)
	(SETQ Z1 (ERRSET (TRYIT)))
   B    (COND ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
					       (EVAL
						(LIST (QUOTE OUTC)
						      (LIST (QUOTE OUTPUT)
							    (QUOTE PRF)
							    (QUOTE DSK:)
							    (CONS (READLIST
								   (CONS (QUOTE N)
									 (CONS (SETQ PRNO (ADD1 PRNO))
 									       FILENAM)))
								  (QUOTE PRF)))
 						      NIL)))
					 (QUERY)
					 (PROOF LHP RHP)
					 (OUTC Z T)
					 (RETURN Z1))
	      ((EQ (CAR Z1) (QUOTE NOPROOF)) (GO A))
	      ((EQ (CAR Z1) (QUOTE ABORT)) (SETQ Z2
						 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))
					   (GO B)))
	(RETURN Z1)
   A    (SETQ Z2 (SETQUERY1 CLAUSES STRAT))
	(SETQ Z1 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
	(GO B))) 
EXPR)